<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Equiv: 程序的等价关系</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 2: 编程语言基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Equiv<span class="subtitle">程序的等价关系</span></h1>


<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Bool.Bool</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.Arith</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Init.Nat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.PeanoNat</span>. <span class="id" type="keyword">Import</span> <span class="id" type="var">Nat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.EqNat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">omega.Omega</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Lists.List</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Logic.FunctionalExtensionality</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">ListNotations</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Imp</span>.<br/>
</div>

<div class="doc">
<a name="lab8"></a><h3 class="section">一些关于习题的建议：</h3>


<div class="paragraph"> </div>

<ul class="doclist">
<li> 这里要进行的大多数 Coq 证明都与我们之前提供的类似。在做作业之前，
      请先花点时间，非形式化地在纸上以及在 Coq 中思考我们的证明，
      确保你完全理解了其中的每个细节。这会节省你大量的时间。

<div class="paragraph"> </div>


</li>
<li> 我们现在进行的 Coq 证明已经足够复杂，几乎不可能再单靠“感觉”
      或乱撞的方式来完成证明了。你需要以“为何某个属性为真”以及“如何进行证明”
      的想法开始。完成此任务的最佳方式是在开始形式化证明前，至少先在纸上写出
      非形式化证明的梗概，即以直观的方式说服自己相信该定理成立，
      然后再进行形式化证明。或者，你也可以拉一个好友，尝试说服他此定理成立，
      然后形式化你的解释。

<div class="paragraph"> </div>


</li>
<li> 请使用自动化工具来减少工作量！如果你全部显式地写出证明中的所有情况，
      那么本章中的证明会非常长。  
</li>
</ul>

</div>

<div class="doc">
<a name="lab9"></a><h1 class="section">行为的等价关系</h1>

<div class="paragraph"> </div>

 在前面的章节中，我们探讨了一个非常简单的程序变换，即 <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span>
    函数的正确性。我们考虑的编程语言为算术表达式语言的第一版，它没有变量，
    因此在该环境下，程序变换正确的意义非常容易定义：它产生的程序的求值结果
    应当总是与原始程序产生的数字相等。

<div class="paragraph"> </div>

    为了讨论整个 Imp 语言中程序变换，特别是赋值的正确性，
    我们需要考虑变量和状态的作用。 
</div>

<div class="doc">
<a name="lab10"></a><h2 class="section">定义</h2>

<div class="paragraph"> </div>

 对于包含变量的 <span class="inlinecode"><span class="id" type="var">aexp</span></span> 和 <span class="inlinecode"><span class="id" type="var">bexp</span></span> 而言，我们所需的定义简单明了。
    只要在所有状态下，两个 <span class="inlinecode"><span class="id" type="var">aexp</span></span> 或 <span class="inlinecode"><span class="id" type="var">bexp</span></span> 的求值结果相同，
    我们就说他们的<b>行为等价（behaviorally equivalent）</b>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">aequiv</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">st</span> : <span class="id" type="var">state</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span> = <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub></span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">bequiv</span> (<span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> : <span class="id" type="var">bexp</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">st</span> : <span class="id" type="var">state</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b<sub>1</sub></span> = <span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b<sub>2</sub></span>.<br/>
</div>

<div class="doc">
下面是一些算术和布尔表达式等价的简单例子。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">aequiv_example</span>: <span class="id" type="var">aequiv</span> (<span class="id" type="var">X</span> - <span class="id" type="var">X</span>) 0.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">bequiv_example</span>: <span class="id" type="var">bequiv</span> (<span class="id" type="var">X</span> - <span class="id" type="var">X</span> = 0)%<span class="id" type="var">imp</span> <span class="id" type="var">true</span>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">beval</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">aequiv_example</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
对指令而言，情况则有些微妙。我们无法简单地说“如果在相同的初始状态下，
    两个指令求值的停机状态相同，那么这两个指令等价”，
    因为有些指令在某些初始状态下运行时根本不会在任何状态下停机！
    我们实际上需要的是：“若两个指令在任何给定的初始状态下，要么发散，
    要么在相同的状态下停机，则二者行为等价。”简单来说，就是：
    “若其中一个指令在某状态下停机，那么另一个也在该状态下停机，反之亦然。” 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">cequiv</span> (<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">st</span> <span class="id" type="var">st'</span> : <span class="id" type="var">state</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span>) ↔ (<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>).<br/>
</div>

<div class="doc">
<a name="lab11"></a><h2 class="section">简单示例</h2>

<div class="paragraph"> </div>

 下面是一些指令等价的例子，我们首先从包含 <span class="inlinecode"><span class="id" type="var">SKIP</span></span> 的简单程序变换开始： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">skip_left</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">SKIP</span>;; <span class="id" type="var">c</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Seq</span> <span class="id" type="keyword">with</span> <span class="id" type="var">st</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab12"></a><h4 class="section">练习：2 星, standard (skip_right)</h4>
 请证明在某条指令之后添加 <span class="inlinecode"><span class="id" type="var">SKIP</span></span> 后，两程序会等价 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">skip_right</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">c</span> ;; <span class="id" type="var">SKIP</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 同样，下面是一个优化 <span class="inlinecode"><span class="id" type="var">TEST</span></span> 的简单程序变换： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">TEST_true_simple</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">true</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfTrue</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
当然，人类程序员是不会写把断言（guard）直接写成 <span class="inlinecode"><span class="id" type="var">true</span></span> 的条件分支的。
    不过当断言<b>等价于真</b>的情况时就会写出来：  <b>定理</b>：若 <span class="inlinecode"><span class="id" type="var">b</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span>，则 <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>。 
<div class="paragraph"> </div>

   <b>证明</b>：

<div class="paragraph"> </div>

<ul class="doclist">
<li> (<span class="inlinecode">→</span>) 我们必须证明，对于所有的 <span class="inlinecode"><span class="id" type="var">st</span></span> 和 <span class="inlinecode"><span class="id" type="var">st'</span></span>，若 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span>
       <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 则 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。

<div class="paragraph"> </div>

       能够应用于 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 的证明规则只有两条：
       <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span> 和 <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span>。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 假设 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 证明自 <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span>
         这条证明规则。若使用证明规则 <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span> 其必备的前提条件 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>
         必为真，而这正好是我们的证明所需要的条件。

<div class="paragraph"> </div>


</li>
<li> 另一方面, 假设 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 证明自
         <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span>。我们能得知 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span> 和 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。

<div class="paragraph"> </div>

         之前提到 <span class="inlinecode"><span class="id" type="var">b</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span>, 即对于所有 <span class="inlinecode"><span class="id" type="var">st</span></span>，有 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span>
         <span class="inlinecode"><span class="id" type="var">BTrue</span></span>。具体来说就是 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span> 成立，因而 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span> <span class="inlinecode">=</span>
         <span class="inlinecode"><span class="id" type="var">true</span></span> 成立。然而，之前假设 <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span> 必备的前提条件 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span>
         也成立，这就构成了一组矛盾，因此不可能使用了 <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span> 这条证明规则。

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> (<span class="inlinecode">&lt;-</span>) 我们必须证明，对于所有 <span class="inlinecode"><span class="id" type="var">st</span></span> 和 <span class="inlinecode"><span class="id" type="var">st'</span></span>，若<span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>
       则 <span class="inlinecode"><span class="id" type="var">IFB</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">\\</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。

<div class="paragraph"> </div>

       已知 <span class="inlinecode"><span class="id" type="var">b</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span>，我们知道 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> = <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span> = <span class="inlinecode"><span class="id" type="var">true</span></span>。
       结合 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 这条假设，我们能应用 <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span> 来证明
       <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。 <span class="proofbox">&#9744;</span>

</li>
</ul>

<div class="paragraph"> </div>

   下面是这个证明的形式化版本： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">TEST_true</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BTrue</span>  →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;b&nbsp;求值为&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;b&nbsp;求值为&nbsp;false（矛盾）&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfTrue</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab13"></a><h4 class="section">练习：2 星, standard, recommended (TEST_false)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">TEST_false</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BFalse</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab14"></a><h4 class="section">练习：3 星, standard (swap_if_branches)</h4>
 证明我们可以通过对断言取反来交换 IF 的两个分支 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">swap_if_branches</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">BNot</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">FI</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 对于 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 循环，我们能够给出一组相似的定理：当循环的断言等价于 <span class="inlinecode"><span class="id" type="var">BFalse</span></span>
    时它等价于 <span class="inlinecode"><span class="id" type="var">SKIP</span></span>；当循环的断言等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span> 时它等价于 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span>
    <span class="inlinecode"><span class="id" type="var">SKIP</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span>（或任意不停机的程序）。前者比较简单。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">WHILE_false</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BFalse</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span>.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileFalse&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileTrue&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileFalse</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab15"></a><h4 class="section">练习：2 星, advanced, optional (WHILE_false_informal)</h4>
 写出 <span class="inlinecode"><span class="id" type="var">WHILE_false</span></span> 的非形式化证明。

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

 为了证明第二个定理，我们需要一个辅助引理：<span class="inlinecode"><span class="id" type="var">WHILE</span></span> 循环在其断言等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span>
    时不会停机。 
<div class="paragraph"> </div>

 <b>引理</b>：若 <span class="inlinecode"><span class="id" type="var">b</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span>，则无法出现
    <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 的情况。

<div class="paragraph"> </div>

    <b>证明</b>：假设 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。我们将证明通过对
    <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 使用归纳法会导出矛盾。需要考虑只有
    <span class="inlinecode"><span class="id" type="var">E_WhileFalse</span></span> 和 <span class="inlinecode"><span class="id" type="var">E_WhileTrue</span></span> 两种情况，其它情况则矛盾。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 假设 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 使用规则 <span class="inlinecode"><span class="id" type="var">E_WhileFalse</span></span> 证明。
        那么根据假设得出 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span>。但它与 <span class="inlinecode"><span class="id" type="var">b</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span> 矛盾。

<div class="paragraph"> </div>


</li>
<li> 假设 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 使用规则 <span class="inlinecode"><span class="id" type="var">E_WhileTrue</span></span>证明。
        我们必有：

</li>
</ul>
      1. <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>，
      2. 存在某个 <span class="inlinecode"><span class="id" type="var">st<sub>0</sub></span></span> 使得 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st<sub>0</sub></span></span> 且
         <span class="inlinecode"><span class="id" type="var">st<sub>0</sub></span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>，
      3. 以及我们给出了导致矛盾的归纳假设 <span class="inlinecode"><span class="id" type="var">st<sub>0</sub></span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>，

<div class="paragraph"> </div>

      我们根据 2 和 3 会得到矛盾。 <span class="proofbox">&#9744;</span> 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">WHILE_true_nonterm</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BTrue</span> →<br/>
&nbsp;&nbsp;~( <span class="id" type="var">st</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st'</span> ).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)%<span class="id" type="var">imp</span> <span class="id" type="keyword">as</span> <span class="id" type="var">cw</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqcw</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>;<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;大多数证明规则无法应用，我们可通过反演（inversion）来去除它们：&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqcw</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">clear</span> <span class="id" type="var">Heqcw</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;我们只关心这两个关于&nbsp;WHILE&nbsp;循环的证明规则：&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_WhileFalse&nbsp;*)</span> <span class="comment">(*&nbsp;矛盾&nbsp;--&nbsp;b&nbsp;总为真！&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;<span class="inlinecode"><span class="id" type="tactic">rewrite</span></span>&nbsp;能实例化&nbsp;<span class="inlinecode"><span class="id" type="var">st</span></span>&nbsp;中的量词&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_WhileTrue&nbsp;*)</span> <span class="comment">(*&nbsp;直接使用&nbsp;IH&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHceval2</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab16"></a><h4 class="section">练习：2 星, standard, optional (WHILE_true_nonterm_informal)</h4>
 试解释 <span class="inlinecode"><span class="id" type="var">WHILE_true_nonterm</span></span> 的含义。

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab17"></a><h4 class="section">练习：2 星, standard, recommended (WHILE_true)</h4>
 请证明以下定理。<b>提示</b>：你可能需要使用 <span class="inlinecode"><span class="id" type="var">WHILE_true_nonterm</span></span> 。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">WHILE_true</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">true</span>  →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> <span class="id" type="var">true</span> <span class="id" type="var">DO</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">END</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 关于 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 指令的更有趣的事实是，任何数量的循环体的副本在不改变意义
    的情况下均可被“展开”。循环展开在实际的编译器中是种常见的变换。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">loop_unrolling</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> (<span class="id" type="var">c</span> ;; <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>) <span class="id" type="var">ELSE</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">FI</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">Hce</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hce</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;不执行循环&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfFalse</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;执行循环&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfTrue</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Seq</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := <span class="id" type="var">st'0</span>). <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hce</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;执行循环&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileTrue</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := <span class="id" type="var">st'0</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;不执行循环&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileFalse</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab18"></a><h4 class="section">练习：2 星, standard, optional (seq_assoc)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">seq_assoc</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>3</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> ((<span class="id" type="var">c<sub>1</sub></span>;;<span class="id" type="var">c<sub>2</sub></span>);;<span class="id" type="var">c<sub>3</sub></span>) (<span class="id" type="var">c<sub>1</sub></span>;;(<span class="id" type="var">c<sub>2</sub></span>;;<span class="id" type="var">c<sub>3</sub></span>)).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 证明涉及赋值的程序的属性经常会用到这一事实，即程序状态会根据其外延性
    （如 <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">;</span> <span class="inlinecode"><span class="id" type="var">m</span></span> 和 <span class="inlinecode"><span class="id" type="var">m</span></span> 是相等的映射）来对待。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">identity_assignment</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">x</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intro</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">t_update_same</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Hx</span> : <span class="id" type="var">st'</span> =[ <span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">x</span> ]⇒ (<span class="id" type="var">x</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">st'</span> <span class="id" type="var">x</span> ; <span class="id" type="var">st'</span>)).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>. <span class="id" type="tactic">reflexivity</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">t_update_same</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hx</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">Hx</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab19"></a><h4 class="section">练习：2 星, standard, recommended (assign_aequiv)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">assign_aequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">x</span> : <span class="id" type="var">string</span>) <span class="id" type="var">e</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">aequiv</span> <span class="id" type="var">x</span> <span class="id" type="var">e</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">SKIP</span> (<span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">e</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab20"></a><h4 class="section">练习：2 星, standard (equiv_classes)</h4>

<div class="paragraph"> </div>

 给定下列程序，请按照它们在 <span class="inlinecode"><span class="id" type="var">Imp</span></span> 中是否等价将这些程序分组。
    你的答案应该是一个列表的列表，其中每个子列表都表示一组等价的程序。
    例如，如果你认为程序 (a) 至 (h) 都互相等价，但不等价于 (i)，那么答案应当如下：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[&nbsp;[<span class="id" type="var">prog_a</span>;<span class="id" type="var">prog_b</span>;<span class="id" type="var">prog_c</span>;<span class="id" type="var">prog_d</span>;<span class="id" type="var">prog_e</span>;<span class="id" type="var">prog_f</span>;<span class="id" type="var">prog_g</span>;<span class="id" type="var">prog_h</span>]&nbsp;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">prog_i</span>]&nbsp;]
<div class="paragraph"> </div>

</div>
    请在 <span class="inlinecode"><span class="id" type="var">equiv_classes</span></span> 的定义下方写出你的答案。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_a</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> ≤ 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_b</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">X</span> = 0 <span class="id" type="var">THEN</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 1<br/>
&nbsp;&nbsp;<span class="id" type="var">ELSE</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0<br/>
&nbsp;&nbsp;<span class="id" type="var">FI</span>;;<br/>
&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> - <span class="id" type="var">Y</span>;;<br/>
&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_c</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">SKIP</span>%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_d</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> (<span class="id" type="var">X</span> * <span class="id" type="var">Y</span>) + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_e</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_f</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1;;<br/>
&nbsp;&nbsp;<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = <span class="id" type="var">Y</span>) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_g</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> <span class="id" type="var">true</span> <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_h</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = <span class="id" type="var">X</span>) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_i</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = <span class="id" type="var">Y</span>) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">Y</span> + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">equiv_classes</span> : <span class="id" type="var">list</span> (<span class="id" type="var">list</span> <span class="id" type="var">com</span>)<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_equiv_classes</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab21"></a><h1 class="section">行为等价的性质</h1>

<div class="paragraph"> </div>

 接下来我们考虑程序等价的一些基本性质。 
</div>

<div class="doc">
<a name="lab22"></a><h2 class="section">行为等价是一种等价关系</h2>

<div class="paragraph"> </div>

 首先, 我们验证 <span class="inlinecode"><span class="id" type="var">aexps</span></span>、<span class="inlinecode"><span class="id" type="var">bexps</span></span> 和 <span class="inlinecode"><span class="id" type="var">com</span></span> 的确满足<b>等价关系（equivalences）</b>
 也就是说，它同时满足自反性（reflexive）、对称性（symmetric）和传递性
      （transitive）。这些证明都很容易。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">refl_aequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>), <span class="id" type="var">aequiv</span> <span class="id" type="var">a</span> <span class="id" type="var">a</span>.<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sym_aequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> → <span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">a<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')"><span class="show"></span></div>
<div class="proofscript" id="proof8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">trans_aequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">a<sub>3</sub></span> : <span class="id" type="var">aexp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> → <span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">a<sub>3</sub></span> → <span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>3</sub></span>.<br/>
<div class="togglescript" id="proofcontrol9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')"><span class="show"></span></div>
<div class="proofscript" id="proof9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">aequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">a<sub>3</sub></span> <span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">H<sub>23</sub></span> <span class="id" type="var">st</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">st</span>). <span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H<sub>23</sub></span> <span class="id" type="var">st</span>). <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">refl_bequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>), <span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">b</span>.<br/>
<div class="togglescript" id="proofcontrol10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')"><span class="show"></span></div>
<div class="proofscript" id="proof10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sym_bequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> : <span class="id" type="var">bexp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> → <span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>2</sub></span> <span class="id" type="var">b<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')"><span class="show"></span></div>
<div class="proofscript" id="proof11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">trans_bequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> <span class="id" type="var">b<sub>3</sub></span> : <span class="id" type="var">bexp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> → <span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>2</sub></span> <span class="id" type="var">b<sub>3</sub></span> → <span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>3</sub></span>.<br/>
<div class="togglescript" id="proofcontrol12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')"><span class="show"></span></div>
<div class="proofscript" id="proof12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> <span class="id" type="var">b<sub>3</sub></span> <span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">H<sub>23</sub></span> <span class="id" type="var">st</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">st</span>). <span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H<sub>23</sub></span> <span class="id" type="var">st</span>). <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">refl_cequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">c</span> : <span class="id" type="var">com</span>), <span class="id" type="var">cequiv</span> <span class="id" type="var">c</span> <span class="id" type="var">c</span>.<br/>
<div class="togglescript" id="proofcontrol13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')"><span class="show"></span></div>
<div class="proofscript" id="proof13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">cequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">iff_refl</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sym_cequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')"><span class="show"></span></div>
<div class="proofscript" id="proof14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">cequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">H</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span> ↔ <span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">H'</span>.<br/>
&nbsp;&nbsp;{ <span class="comment">(*&nbsp;Proof&nbsp;of&nbsp;assertion&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_sym</span>. <span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">iff_trans</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P<sub>1</sub></span> <span class="id" type="var">P<sub>2</sub></span> <span class="id" type="var">P<sub>3</sub></span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span class="id" type="var">P<sub>1</sub></span> ↔ <span class="id" type="var">P<sub>2</sub></span>) → (<span class="id" type="var">P<sub>2</sub></span> ↔ <span class="id" type="var">P<sub>3</sub></span>) → (<span class="id" type="var">P<sub>1</sub></span> ↔ <span class="id" type="var">P<sub>3</sub></span>).<br/>
<div class="togglescript" id="proofcontrol15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')"><span class="show"></span></div>
<div class="proofscript" id="proof15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">P<sub>1</sub></span> <span class="id" type="var">P<sub>2</sub></span> <span class="id" type="var">P<sub>3</sub></span> <span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">H<sub>23</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>12</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>23</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">A</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>1</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">A</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>0</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">A</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">trans_cequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>3</sub></span> : <span class="id" type="var">com</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>3</sub></span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>3</sub></span>.<br/>
<div class="togglescript" id="proofcontrol16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')"><span class="show"></span></div>
<div class="proofscript" id="proof16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">cequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>3</sub></span> <span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">H<sub>23</sub></span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_trans</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>). <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>12</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>23</sub></span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab23"></a><h2 class="section">行为等价是一种一致性</h2>

<div class="paragraph"> </div>

 虽然不太明显，但行为等价也满足<b>一致性（congruence）</b>。
    即，如果两个子程序等价，那么当二者所在的更大的程序中只有二者不同时，
    这两个更大的程序也等价：
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">aequiv&nbsp;a<sub>1</sub>&nbsp;a<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">cequiv&nbsp;(x&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;a<sub>1</sub>)&nbsp;(x&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;a<sub>1</sub>')</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">cequiv&nbsp;c<sub>1</sub>&nbsp;c<sub>1</sub>'</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">cequiv&nbsp;c<sub>2</sub>&nbsp;c<sub>2</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">cequiv&nbsp;(c<sub>1</sub>;;c<sub>2</sub>)&nbsp;(c<sub>1</sub>';;c<sub>2</sub>')</td>
  <td></td>
</td>
</table></center>    ...以及这些指令的更多其它形式。 
<div class="paragraph"> </div>

 （注意这里使用的推理规则的记法并不是定义的成部分，只是将一些
    合法的蕴含式用易读的方式写下而已。接下来我们将证明这些蕴含式。） 
<div class="paragraph"> </div>

 在接下来的章节（<span class="inlinecode"><span class="id" type="var">fold_constants_com_sound</span></span> 的证明）中，我们会用
    具体例子来说明这种一致性多么重要。不过它最主要意义在于，当我们在用
    一小部分程序替换大程序中等价的部分并证明替换前后程序的等价关系时，
    <b>无需</b>进行与不变的部分相关的证明。也就是说，程序的改变所产生的证明的工作量
    与改变的大小而非整个程序的大小成比例。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">CAss_congruence</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>1</sub>'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> (<span class="id" type="var">CAss</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span>) (<span class="id" type="var">CAss</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub>'</span>).<br/>
<div class="togglescript" id="proofcontrol17" onclick="toggleDisplay('proof17');toggleDisplay('proofcontrol17')"><span class="show"></span></div>
<div class="proofscript" id="proof17" onclick="toggleDisplay('proof17');toggleDisplay('proofcontrol17')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">Heqv</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">Hceval</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hceval</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Heqv</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hceval</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Heqv</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
循环的一致性更有趣, 因为它需要使用归纳法。

<div class="paragraph"> </div>

    <b>定理</b>: 对于 <span class="inlinecode"><span class="id" type="var">WHILE</span></span>，等价关系是一种一致性 &mdash; 即，若 <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> 等价于 <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> 且 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>
    等价于 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span>，那么 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span>。

<div class="paragraph"> </div>

    <b>证明</b>: 假设 <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> 等价于 <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> 且 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> 等价于 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span>。我们必须证明，
    对于每个 <span class="inlinecode"><span class="id" type="var">st</span></span> 和 <span class="inlinecode"><span class="id" type="var">st'</span></span>，<span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 当且仅当
    <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。我们把两个方向分开考虑。

<div class="paragraph"> </div>

<ul class="doclist">
<li> (<span class="inlinecode">→</span>) 我们通过对 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 使用归纳法证明
        <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 蕴含 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。
        只有推导的最后所使用的规则为 <span class="inlinecode"><span class="id" type="var">E_WhileFalse</span></span> 或 <span class="inlinecode"><span class="id" type="var">E_WhileTrue</span></span>
        时才需要进行特别讨论。

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">E_WhileFalse</span></span>：此时我们拥有假设的必备条件 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span>
            和 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。但是，由于 <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> 等价，我们有
            <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span>，然后应用 <span class="inlinecode"><span class="id" type="var">E</span>-<span class="id" type="var">WhileFalse</span></span> 得出我们需要的
            <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="var">E_WhileTrue</span></span>：此时我们拥有假设的必备条件 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>，以及
            对于某些状态 <span class="inlinecode"><span class="id" type="var">st'0</span></span> 的 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'0</span></span> 和 <span class="inlinecode"><span class="id" type="var">st'0</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>
            <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>，还有归纳假设 <span class="inlinecode"><span class="id" type="var">st'0</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。

<div class="paragraph"> </div>

            由于 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> 等价，我们有 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'0</span></span>；
            由于 <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> 等价，我们有 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>。现在应用
            <span class="inlinecode"><span class="id" type="var">E</span>-<span class="id" type="var">WhileTrue</span></span>，得出我们所需的 <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>。

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> (<span class="inlinecode">&lt;-</span>) 反之亦然。 <span class="proofbox">&#9744;</span> 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">CWhile_congruence</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>1</sub>'</span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">DO</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">END</span>) (<span class="id" type="var">WHILE</span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">DO</span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">END</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>,<span class="id" type="var">cequiv</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">Hb1e</span> <span class="id" type="var">Hc1e</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">Hce</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">DO</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">END</span>)%<span class="id" type="var">imp</span> <span class="id" type="keyword">as</span> <span class="id" type="var">cwhile</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">eqn</span>:<span class="id" type="var">Heqcwhile</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hce</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqcwhile</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileFalse&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileFalse</span>. <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">Hb1e</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileTrue&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileTrue</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := <span class="id" type="var">st'</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;执行展示循环&nbsp;*)</span> <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">Hb1e</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;执行主体&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">Hc1e</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>). <span class="id" type="tactic">apply</span> <span class="id" type="var">Hce1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;执行之后的循环&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHHce2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">DO</span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">END</span>)%<span class="id" type="var">imp</span> <span class="id" type="keyword">as</span> <span class="id" type="var">c'while</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">eqn</span>:<span class="id" type="var">Heqc'while</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hce</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqc'while</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileFalse&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileFalse</span>. <span class="id" type="tactic">rewrite</span> → <span class="id" type="var">Hb1e</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileTrue&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileTrue</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := <span class="id" type="var">st'</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;执行展示循环&nbsp;*)</span> <span class="id" type="tactic">rewrite</span> → <span class="id" type="var">Hb1e</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;执行主体&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">Hc1e</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>). <span class="id" type="tactic">apply</span> <span class="id" type="var">Hce1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;执行之后的循环&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHHce2</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab24"></a><h4 class="section">练习：3 星, standard, optional (CSeq_congruence)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">CSeq_congruence</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>2</sub>'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>2</sub>'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> (<span class="id" type="var">c<sub>1</sub></span>;;<span class="id" type="var">c<sub>2</sub></span>) (<span class="id" type="var">c<sub>1</sub>'</span>;;<span class="id" type="var">c<sub>2</sub>'</span>).<br/>
<div class="togglescript" id="proofcontrol18" onclick="toggleDisplay('proof18');toggleDisplay('proofcontrol18')"><span class="show"></span></div>
<div class="proofscript" id="proof18" onclick="toggleDisplay('proof18');toggleDisplay('proofcontrol18')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<br/>
</div>

<div class="doc">
<a name="lab25"></a><h4 class="section">练习：3 星, standard (CIf_congruence)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">CIf_congruence</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">b'</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>2</sub>'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">b'</span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>2</sub>'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> (<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">b'</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub>'</span> <span class="id" type="var">FI</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 例如，下面是两个等价的程序和它们等价关系的证明... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">congruence_example</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;程序&nbsp;1：&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> <span class="id" type="var">X</span> = 0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">THEN</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 42<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;程序&nbsp;1：&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> <span class="id" type="var">X</span> = 0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">THEN</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> - <span class="id" type="var">X</span>   <span class="comment">(*&nbsp;&lt;---&nbsp;这里不同&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 42<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">FI</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">CSeq_congruence</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">refl_cequiv</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">CIf_congruence</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">refl_bequiv</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">CAss_congruence</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">aequiv</span>. <span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">minus_diag</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">refl_cequiv</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab26"></a><h4 class="section">练习：3 星, advanced, optional (not_congr)</h4>
 我们已经证明了 <span class="inlinecode"><span class="id" type="var">cequiv</span></span> 关系对指令同时满足等价关系和一致性。
    你能想出一个对于指令满足等价关系但<b>不满足</b>一致性的关系吗？ 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab27"></a><h1 class="section">程序变换</h1>

<div class="paragraph"> </div>

 <b>程序变换（program transformation）</b>是一种以某个程序作为输入，
    产生该程序的某种变体作为输出的函数。编译器优化中的常量折叠就是个经典的例子，
    然而程序变换并不仅限如此。 
<div class="paragraph"> </div>

 如果一个程序变换保留了其原始行为，那么它就是<b>可靠（sound）</b>的。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">atrans_sound</span> (<span class="id" type="var">atrans</span> : <span class="id" type="var">aexp</span> → <span class="id" type="var">aexp</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aequiv</span> <span class="id" type="var">a</span> (<span class="id" type="var">atrans</span> <span class="id" type="var">a</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">btrans_sound</span> (<span class="id" type="var">btrans</span> : <span class="id" type="var">bexp</span> → <span class="id" type="var">bexp</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> (<span class="id" type="var">btrans</span> <span class="id" type="var">b</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">ctrans_sound</span> (<span class="id" type="var">ctrans</span> : <span class="id" type="var">com</span> → <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">c</span> : <span class="id" type="var">com</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">c</span> (<span class="id" type="var">ctrans</span> <span class="id" type="var">c</span>).<br/>
</div>

<div class="doc">
<a name="lab28"></a><h2 class="section">常量折叠变换</h2>

<div class="paragraph"> </div>

 不引用变量的表达式为<b>常量（constant）</b>。

<div class="paragraph"> </div>

    常量折叠是一种找到常量表达式并把它们替换为其值的优化方法。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">fold_constants_aexp</span> (<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>) : <span class="id" type="var">aexp</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">a</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> <span class="id" type="var">n</span>       ⇒ <span class="id" type="var">ANum</span> <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">AId</span> <span class="id" type="var">x</span>        ⇒ <span class="id" type="var">AId</span> <span class="id" type="var">x</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>1</sub></span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>2</sub></span>) ⇒ <span class="id" type="var">ANum</span> (<span class="id" type="var">n<sub>1</sub></span> + <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a<sub>1</sub>'</span>, <span class="id" type="var">a<sub>2</sub>'</span>) ⇒ <span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">a<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>1</sub></span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>2</sub></span>) ⇒ <span class="id" type="var">ANum</span> (<span class="id" type="var">n<sub>1</sub></span> - <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a<sub>1</sub>'</span>, <span class="id" type="var">a<sub>2</sub>'</span>) ⇒ <span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">a<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>1</sub></span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>2</sub></span>) ⇒ <span class="id" type="var">ANum</span> (<span class="id" type="var">n<sub>1</sub></span> * <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a<sub>1</sub>'</span>, <span class="id" type="var">a<sub>2</sub>'</span>) ⇒ <span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">a<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_aexp_ex<sub>1</sub></span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> ((1 + 2) * <span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;= (3 * <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span>.<br/>
<div class="togglescript" id="proofcontrol19" onclick="toggleDisplay('proof19');toggleDisplay('proofcontrol19')"><span class="show"></span></div>
<div class="proofscript" id="proof19" onclick="toggleDisplay('proof19');toggleDisplay('proofcontrol19')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
注意此版本的常量折叠不包括优化平凡的加法等 &mdash; 为简单起见，
    我们把注意力集中到单个优化上来。将其它简化表达式的方法加进来也不难，
    只是定义和证明会更长。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_aexp_ex<sub>2</sub></span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> (<span class="id" type="var">X</span> - ((0 * 6) + <span class="id" type="var">Y</span>))%<span class="id" type="var">imp</span> = (<span class="id" type="var">X</span> - (0 + <span class="id" type="var">Y</span>))%<span class="id" type="var">imp</span>.<br/>
<div class="togglescript" id="proofcontrol20" onclick="toggleDisplay('proof20');toggleDisplay('proofcontrol20')"><span class="show"></span></div>
<div class="proofscript" id="proof20" onclick="toggleDisplay('proof20');toggleDisplay('proofcontrol20')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
我们不仅可以将 <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span> 优化成 <span class="inlinecode"><span class="id" type="var">bexp</span></span>（如在 <span class="inlinecode"><span class="id" type="var">BEq</span></span> 和 <span class="inlinecode"><span class="id" type="var">BLe</span></span>
    的情况下），还可以查找常量<b>布尔</b>表达式并原地求值。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">fold_constants_bexp</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) : <span class="id" type="var">bexp</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">b</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BTrue</span>        ⇒ <span class="id" type="var">BTrue</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BFalse</span>       ⇒ <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BEq</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>) <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>1</sub></span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>2</sub></span>) ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">n<sub>1</sub></span> =? <span class="id" type="var">n<sub>2</sub></span> <span class="id" type="keyword">then</span> <span class="id" type="var">BTrue</span> <span class="id" type="keyword">else</span> <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a<sub>1</sub>'</span>, <span class="id" type="var">a<sub>2</sub>'</span>) ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">BEq</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">a<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BLe</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>) <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>1</sub></span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>2</sub></span>) ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">n<sub>1</sub></span> &lt;=? <span class="id" type="var">n<sub>2</sub></span> <span class="id" type="keyword">then</span> <span class="id" type="var">BTrue</span> <span class="id" type="keyword">else</span> <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a<sub>1</sub>'</span>, <span class="id" type="var">a<sub>2</sub>'</span>) ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">BLe</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">a<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BNot</span> <span class="id" type="var">b<sub>1</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b<sub>1</sub></span>) <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BTrue</span> ⇒ <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BFalse</span> ⇒ <span class="id" type="var">BTrue</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">b<sub>1</sub>'</span> ⇒ <span class="id" type="var">BNot</span> <span class="id" type="var">b<sub>1</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BAnd</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b<sub>2</sub></span>) <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">BTrue</span>, <span class="id" type="var">BTrue</span>) ⇒ <span class="id" type="var">BTrue</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">BTrue</span>, <span class="id" type="var">BFalse</span>) ⇒ <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">BFalse</span>, <span class="id" type="var">BTrue</span>) ⇒ <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">BFalse</span>, <span class="id" type="var">BFalse</span>) ⇒ <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">b<sub>1</sub>'</span>, <span class="id" type="var">b<sub>2</sub>'</span>) ⇒ <span class="id" type="var">BAnd</span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">b<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_bexp_ex<sub>1</sub></span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold_constants_bexp</span> (<span class="id" type="var">true</span> &amp;&amp; ~(<span class="id" type="var">false</span> &amp;&amp; <span class="id" type="var">true</span>))%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;= <span class="id" type="var">true</span>.<br/>
<div class="togglescript" id="proofcontrol21" onclick="toggleDisplay('proof21');toggleDisplay('proofcontrol21')"><span class="show"></span></div>
<div class="proofscript" id="proof21" onclick="toggleDisplay('proof21');toggleDisplay('proofcontrol21')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_bexp_ex<sub>2</sub></span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold_constants_bexp</span> ((<span class="id" type="var">X</span> = <span class="id" type="var">Y</span>) &amp;&amp; (0 = (2 - (1 + 1))))%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;= ((<span class="id" type="var">X</span> = <span class="id" type="var">Y</span>) &amp;&amp; <span class="id" type="var">true</span>)%<span class="id" type="var">imp</span>.<br/>
<div class="togglescript" id="proofcontrol22" onclick="toggleDisplay('proof22');toggleDisplay('proofcontrol22')"><span class="show"></span></div>
<div class="proofscript" id="proof22" onclick="toggleDisplay('proof22');toggleDisplay('proofcontrol22')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
为了折叠指令中的常量，我们需要对所有内嵌的表达式应用适当的折叠函数。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp</span>.<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">fold_constants_com</span> (<span class="id" type="var">c</span> : <span class="id" type="var">com</span>) : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">c</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">SKIP</span>      ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a</span>   ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">c<sub>1</sub></span> ;; <span class="id" type="var">c<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>1</sub></span>) ;; (<span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BTrue</span>  ⇒ <span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>1</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BFalse</span> ⇒ <span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">b'</span> ⇒ <span class="id" type="var">TEST</span> <span class="id" type="var">b'</span> <span class="id" type="var">THEN</span> <span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>1</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span> <span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BTrue</span> ⇒ <span class="id" type="var">WHILE</span> <span class="id" type="var">BTrue</span> <span class="id" type="var">DO</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">END</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BFalse</span> ⇒ <span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">b'</span> ⇒ <span class="id" type="var">WHILE</span> <span class="id" type="var">b'</span> <span class="id" type="var">DO</span> (<span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c</span>) <span class="id" type="var">END</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
<span class="id" type="var">Close</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_com_ex<sub>1</sub></span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold_constants_com</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;原程序：&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 4 + 5;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> - 3;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> (<span class="id" type="var">X</span> - <span class="id" type="var">Y</span>) = (2 + 4) <span class="id" type="var">THEN</span> <span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span> <span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0 <span class="id" type="var">FI</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> 0 ≤ (4 - (2 + 1)) <span class="id" type="var">THEN</span> <span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">FI</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">WHILE</span> <span class="id" type="var">Y</span> = 0 <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;= <span class="comment">(*&nbsp;常量折叠后：&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 9;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> - 3;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> (<span class="id" type="var">X</span> - <span class="id" type="var">Y</span>) = 6 <span class="id" type="var">THEN</span> <span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span> <span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0 <span class="id" type="var">FI</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">WHILE</span> <span class="id" type="var">Y</span> = 0 <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/>
<div class="togglescript" id="proofcontrol23" onclick="toggleDisplay('proof23');toggleDisplay('proofcontrol23')"><span class="show"></span></div>
<div class="proofscript" id="proof23" onclick="toggleDisplay('proof23');toggleDisplay('proofcontrol23')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab29"></a><h2 class="section">常量折叠的可靠性</h2>

<div class="paragraph"> </div>

 现在我们需要证明之前所做事情的正确性。 
<div class="paragraph"> </div>

 下面是对算术表达式的证明： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">fold_constants_aexp_sound</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">atrans_sound</span> <span class="id" type="var">fold_constants_aexp</span>.<br/>
<div class="togglescript" id="proofcontrol24" onclick="toggleDisplay('proof24');toggleDisplay('proofcontrol24')"><span class="show"></span></div>
<div class="proofscript" id="proof24" onclick="toggleDisplay('proof24');toggleDisplay('proofcontrol24')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">atrans_sound</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">a</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">aequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>; <span class="id" type="tactic">simpl</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;ANum&nbsp;和&nbsp;AId&nbsp;很显然&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;从&nbsp;IH&nbsp;和下面的观察出发很容易完成对&nbsp;APlus、AMinus&nbsp;和&nbsp;AMult&nbsp;情况的证明：<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;aeval&nbsp;st&nbsp;(APlus&nbsp;a<sub>1</sub>&nbsp;a<sub>2</sub>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;ANum&nbsp;((aeval&nbsp;st&nbsp;a<sub>1</sub>)&nbsp;+&nbsp;(aeval&nbsp;st&nbsp;a<sub>2</sub>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;aeval&nbsp;st&nbsp;(ANum&nbsp;((aeval&nbsp;st&nbsp;a<sub>1</sub>)&nbsp;+&nbsp;(aeval&nbsp;st&nbsp;a<sub>2</sub>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;（AMinus/minus&nbsp;和&nbsp;AMult/mult&nbsp;同理）&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> (<span class="id" type="tactic">destruct</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>). <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab30"></a><h4 class="section">练习：3 星, standard, optional (fold_bexp_Eq_informal)</h4>
 下面是布尔表达式常量折叠中 <span class="inlinecode"><span class="id" type="var">BEq</span></span> 情况的可靠性的证明。
    请认真读完它再和之后的形式化证明作比较，然后补充完 <span class="inlinecode"><span class="id" type="var">BLe</span></span> 情况的形式化证明
    （尽量不看之前 <span class="inlinecode"><span class="id" type="var">BEq</span></span> 情况的证明）。

<div class="paragraph"> </div>

   <b>定理</b>：布尔值的常量折叠函数 <span class="inlinecode"><span class="id" type="var">fold_constants_bexp</span></span> 是可靠的。

<div class="paragraph"> </div>

   <b>证明</b>：我们必须证明对于所有的布尔表达式 <span class="inlinecode"><span class="id" type="var">b</span></span>，<span class="inlinecode"><span class="id" type="var">b</span></span> 都等价于
   <span class="inlinecode"><span class="id" type="var">fold_constants_bexp</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span>。我们对 <span class="inlinecode"><span class="id" type="var">b</span></span> 使用归纳法。这里只给出了 <span class="inlinecode"><span class="id" type="var">b</span></span>
   形如 <span class="inlinecode"><span class="id" type="var">BEq</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span> 的情况。

<div class="paragraph"> </div>

   在本情况中，我们必须证明

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_bexp</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)).
<div class="paragraph"> </div>

</div>
   有两种情况需要考虑：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 首先，假设对于某些 <span class="inlinecode"><span class="id" type="var">n<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">n<sub>2</sub></span></span> 而言有 <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n<sub>1</sub></span></span>
       和 <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n<sub>2</sub></span></span>。

<div class="paragraph"> </div>

       在此情况下，我们有

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_bexp</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">BTrue</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">BFalse</span>
<div class="paragraph"> </div>

</div>
       和

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)&nbsp;=?&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>).
<div class="paragraph"> </div>

</div>
       根据算术表达式常量折叠的健全性（引理 <span class="inlinecode"><span class="id" type="var">fold_constants_aexp_sound</span></span>）可得

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span><br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">ANum</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">n<sub>1</sub></span>
<div class="paragraph"> </div>

</div>
       和

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span><br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">ANum</span>&nbsp;<span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">n<sub>2</sub></span>,
<div class="paragraph"> </div>

</div>
       因此

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)&nbsp;=?&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>.
<div class="paragraph"> </div>

</div>
       此外，在分别考虑 <span class="inlinecode"><span class="id" type="var">n<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n<sub>2</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">n<sub>1</sub></span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" type="var">n<sub>2</sub></span></span> 的情况后，容易看出

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">BTrue</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">BFalse</span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">BTrue</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">true</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">false</span><br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>.
<div class="paragraph"> </div>

</div>
       因此

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>.<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">BTrue</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">BFalse</span>),
<div class="paragraph"> </div>

</div>
       正是所需的假设。

<div class="paragraph"> </div>


</li>
<li> 另一方面，假设 <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span>
       之一并非常量。此时，我们必须证明

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)),
<div class="paragraph"> </div>

</div>
       根据 <span class="inlinecode"><span class="id" type="var">beval</span></span> 的定义，它等同于证明

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)&nbsp;=?&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>))&nbsp;=?<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)).
<div class="paragraph"> </div>

</div>
       但是，由于算术表达式的可靠性（定理 <span class="inlinecode"><span class="id" type="var">fold_constants_aexp_sound</span></span>）可得出

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>),
<div class="paragraph"> </div>

</div>
       本例证毕。  <span class="proofbox">&#9744;</span> 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">fold_constants_bexp_sound</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">btrans_sound</span> <span class="id" type="var">fold_constants_bexp</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">btrans_sound</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">b</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;BTrue&nbsp;和&nbsp;BFalse&nbsp;是显然的&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;BEq&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
</div>

<div class="doc">
（当存在许多构造子时，使用归纳法会让给变量取名编程一件琐事，
    然而 Coq 并不总是能够选择足够好的变量名。我们可以使用 <span class="inlinecode"><span class="id" type="tactic">rename</span></span> 重命名：
    策略 <span class="inlinecode"><span class="id" type="tactic">rename</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode"><span class="id" type="var">into</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> 会将当前目标和上下文中的 <span class="inlinecode"><span class="id" type="var">a</span></span> 重命名为 <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span>。） 
</div>
<div class="code code-tight">

&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqa1'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">a<sub>2</sub>'</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqa2'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">replace</span> (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span>) <span class="id" type="keyword">with</span> (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub>'</span>) <span class="id" type="tactic">by</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">subst</span> <span class="id" type="var">a<sub>1</sub>'</span>; <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">fold_constants_aexp_sound</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">replace</span> (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub></span>) <span class="id" type="keyword">with</span> (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub>'</span>) <span class="id" type="tactic">by</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">subst</span> <span class="id" type="var">a<sub>2</sub>'</span>; <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">fold_constants_aexp_sound</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">a<sub>1</sub>'</span>; <span class="id" type="tactic">destruct</span> <span class="id" type="var">a<sub>2</sub>'</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;唯一有趣的是&nbsp;a<sub>1</sub>&nbsp;和&nbsp;a<sub>2</sub>&nbsp;在折叠后同时变为常量&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">n</span> =? <span class="id" type="var">n<sub>0</sub></span>); <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;BLe&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">admit</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;BNot&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="var">remember</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">b'</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqb'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">b'</span>; <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;BAnd&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b<sub>1</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqb1'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b<sub>2</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">b<sub>2</sub>'</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqb2'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHb1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHb2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">b<sub>1</sub>'</span>; <span class="id" type="tactic">destruct</span> <span class="id" type="var">b<sub>2</sub>'</span>; <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab31"></a><h4 class="section">练习：3 星, standard (fold_constants_com_sound)</h4>
 完成以下证明的 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 情况。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">fold_constants_com_sound</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">ctrans_sound</span> <span class="id" type="var">fold_constants_com</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">ctrans_sound</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">c</span>; <span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;SKIP&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">refl_cequiv</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">CAss_congruence</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">fold_constants_aexp_sound</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;;;&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">CSeq_congruence</span>; <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;TEST&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b</span>)). {<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">fold_constants_bexp_sound</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b</span>) <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqb</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> (<span class="id" type="tactic">apply</span> <span class="id" type="var">CIf_congruence</span>; <span class="id" type="tactic">assumption</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;（如果&nbsp;if&nbsp;没有被优化掉，那么我们很容易使用&nbsp;IH&nbsp;和<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="var">fold_constants_bexp_sound</span></span>&nbsp;来得出证明。）&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;b&nbsp;总为真&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">trans_cequiv</span> <span class="id" type="keyword">with</span> <span class="id" type="var">c<sub>1</sub></span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">TEST_true</span>; <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;b&nbsp;总为假&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">trans_cequiv</span> <span class="id" type="keyword">with</span> <span class="id" type="var">c<sub>2</sub></span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">TEST_false</span>; <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;WHILE&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab32"></a><h3 class="section">再论 (0 + n) 优化的可靠性</h3>

<div class="paragraph"> </div>

<a name="lab33"></a><h4 class="section">练习：4 星, advanced, optional (optimize_0plus)</h4>
 回顾<b>逻辑基础</b> <a href="https://coq-zh.github.io/SF-zh/lf-current/Imp.html"><span class="inlineref">Imp</span></a> 一章中 <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> 的定义：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Fixpoint</span>&nbsp;<span class="id" type="var">optimize_0plus</span>&nbsp;(<span class="id" type="var">e</span>:<span class="id" type="var">aexp</span>)&nbsp;:&nbsp;<span class="id" type="var">aexp</span>&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span>&nbsp;<span class="id" type="var">e</span>&nbsp;<span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ANum</span>&nbsp;<span class="id" type="var">n</span>&nbsp;⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ANum</span>&nbsp;<span class="id" type="var">n</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">APlus</span>&nbsp;(<span class="id" type="var">ANum</span>&nbsp;0)&nbsp;<span class="id" type="var">e<sub>2</sub></span>&nbsp;⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">APlus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>&nbsp;⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">APlus</span>&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>)&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">AMinus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>&nbsp;⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">AMinus</span>&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>)&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">AMult</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>&nbsp;⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">AMult</span>&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>)&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span>.
<div class="paragraph"> </div>

</div>
   注意此函数是针对无状态的 <span class="inlinecode"><span class="id" type="var">aexp</span></span> 编写的。

<div class="paragraph"> </div>

   请为 <span class="inlinecode"><span class="id" type="var">aexp</span></span> <span class="inlinecode"><span class="id" type="var">bexp</span></span> 和 <span class="inlinecode"><span class="id" type="var">com</span></span> 都写一个带状态的新版本：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">optimize_0plus_aexp</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">optimize_0plus_bexp</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">optimize_0plus_com</span>
<div class="paragraph"> </div>

</div>
   请证明这三个函数都具有可靠性，就像之前证明 <span class="inlinecode"><span class="id" type="var">fold_constants_</span>*</span> 那样。在
   <span class="inlinecode"><span class="id" type="var">optimize_0plus_com</span></span> 的证明中你需要一致性引理 &mdash; 否则证明过程会<b>很长</b>！

<div class="paragraph"> </div>

   接下来为指令定义一个优化器，它首先使用常量折叠（<span class="inlinecode"><span class="id" type="var">fold_constants_com</span></span>）然后优化掉
   <span class="inlinecode">0</span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">n</span></span> 项（使用 <span class="inlinecode"><span class="id" type="var">optimize_0plus_com</span></span>）。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 请为此优化器写一个有意义的测试用例。

<div class="paragraph"> </div>


</li>
<li> 证明此优化程序有可靠性。（这部分应该会<b>很简单</b> 。）  
</li>
</ul>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab34"></a><h1 class="section">证明程序不等价</h1>

<div class="paragraph"> </div>

 假设 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> 是形如 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span>;;</span> <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span> 的指令，并且 <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> 是形如
    <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span>;;</span> <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub>'</span></span> 的指令，<span class="inlinecode"><span class="id" type="var">a<sub>2</sub>'</span></span> 是把 <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span> 中所有 <span class="inlinecode"><span class="id" type="var">X</span></span> 都替换为 <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span>
    后的结果。比如，<span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> 可以像这样：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>1</sub></span>&nbsp;&nbsp;=&nbsp;&nbsp;(<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;42&nbsp;+&nbsp;53;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;+&nbsp;<span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>2</sub></span>&nbsp;&nbsp;=&nbsp;&nbsp;(<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;42&nbsp;+&nbsp;53;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;+&nbsp;(42&nbsp;+&nbsp;53))
<div class="paragraph"> </div>

</div>
    很明显，在这个<b>特定的例子中</b> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> 是等价的。但是对一般程序而言，
    此结果是否成立？ 
<div class="paragraph"> </div>

 我们马上就会发现这是不行的。不过且慢，现在，
    看你自己能否找出一个反例来。 
<div class="paragraph"> </div>

 以下形式化的定义描述了如何在算术表达式 <span class="inlinecode"><span class="id" type="var">a</span></span> 中，
    将某个变量 <span class="inlinecode"><span class="id" type="var">x</span></span> 的所有引用都替换成另一个表达式 <span class="inlinecode"><span class="id" type="var">u</span></span> ： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">subst_aexp</span> (<span class="id" type="var">x</span> : <span class="id" type="var">string</span>) (<span class="id" type="var">u</span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>) : <span class="id" type="var">aexp</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">a</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> <span class="id" type="var">n</span>       ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ANum</span> <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">AId</span> <span class="id" type="var">x'</span>       ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">eqb_string</span> <span class="id" type="var">x</span> <span class="id" type="var">x'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">u</span> <span class="id" type="keyword">else</span> <span class="id" type="var">AId</span> <span class="id" type="var">x'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">APlus</span> (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>1</sub></span>) (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">AMinus</span> (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>1</sub></span>) (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">AMult</span> (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>1</sub></span>) (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">subst_aexp_ex</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">subst_aexp</span> <span class="id" type="var">X</span> (42 + 53) (<span class="id" type="var">Y</span> + <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;= (<span class="id" type="var">Y</span> + (42 + 53))%<span class="id" type="var">imp</span>.<br/>
<div class="togglescript" id="proofcontrol25" onclick="toggleDisplay('proof25');toggleDisplay('proofcontrol25')"><span class="show"></span></div>
<div class="proofscript" id="proof25" onclick="toggleDisplay('proof25');toggleDisplay('proofcontrol25')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
而这里是一个我们感兴趣的性质：它断言类似上述形式的 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span>
    总是等价的。  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">subst_equiv_property</span> := <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x<sub>1</sub></span> <span class="id" type="var">x<sub>2</sub></span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> (<span class="id" type="var">x<sub>1</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span>;; <span class="id" type="var">x<sub>2</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x<sub>1</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span>;; <span class="id" type="var">x<sub>2</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">subst_aexp</span> <span class="id" type="var">x<sub>1</sub></span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>).<br/>
</div>

<div class="doc">
遗憾的是, 这个性质<b>并不</b>总是成立 &mdash; 即，它并不是对所有的
    <span class="inlinecode"><span class="id" type="var">x<sub>1</sub></span></span>、<span class="inlinecode"><span class="id" type="var">x<sub>2</sub></span></span>、<span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span> 都成立。

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">cequiv</span>&nbsp;(<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>;;&nbsp;<span class="id" type="var">x<sub>2</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>;;&nbsp;<span class="id" type="var">x<sub>2</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">subst_aexp</span>&nbsp;<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>).
<div class="paragraph"> </div>

</div>
    我们使用反证法来证明这一点。假设对于所有的 <span class="inlinecode"><span class="id" type="var">x<sub>1</sub></span></span>、<span class="inlinecode"><span class="id" type="var">x<sub>2</sub></span></span>、<span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span>
    和 <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span>，我们有

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">cequiv</span>&nbsp;(<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>;;&nbsp;<span class="id" type="var">x<sub>2</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>;;&nbsp;<span class="id" type="var">x<sub>2</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">subst_aexp</span>&nbsp;<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>).
<div class="paragraph"> </div>

</div>
    考虑以下程序：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>
<div class="paragraph"> </div>

</div>
    注意

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty_st</span>&nbsp;=[&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;]⇒&nbsp;<span class="id" type="var">st<sub>1</sub></span>,
<div class="paragraph"> </div>

</div>
    其中 <span class="inlinecode"><span class="id" type="var">st<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode">(<span class="id" type="var">Y</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">1</span> <span class="inlinecode">;</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">1)</span>.

<div class="paragraph"> </div>

    根据假设，我们知道

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">cequiv</span>&nbsp;(<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1)
<div class="paragraph"> </div>

</div>
    同时，根据 <span class="inlinecode"><span class="id" type="var">cequiv</span></span> 的定义，我们有

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty_st</span>&nbsp;=[&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1&nbsp;]⇒&nbsp;<span class="id" type="var">st<sub>1</sub></span>.
<div class="paragraph"> </div>

</div>
    但是我们也能推导出

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty_st</span>&nbsp;=[&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1&nbsp;]⇒&nbsp;<span class="id" type="var">st<sub>2</sub></span>,
<div class="paragraph"> </div>

</div>
    其中 <span class="inlinecode"><span class="id" type="var">st<sub>2</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode">(<span class="id" type="var">Y</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">2</span> <span class="inlinecode">;</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">1)</span>。但由于 <span class="inlinecode"><span class="id" type="var">ceval</span></span> 是确定性的，而
    <span class="inlinecode"><span class="id" type="var">st<sub>1</sub></span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" type="var">st<sub>2</sub></span></span> ，这就造成了矛盾！  <span class="proofbox">&#9744;</span> 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">subst_inequiv</span> :<br/>
&nbsp;&nbsp;¬<span class="id" type="var">subst_equiv_property</span>.<br/>
<div class="togglescript" id="proofcontrol26" onclick="toggleDisplay('proof26');toggleDisplay('proofcontrol26')"><span class="show"></span></div>
<div class="proofscript" id="proof26" onclick="toggleDisplay('proof26');toggleDisplay('proofcontrol26')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">subst_equiv_property</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Contra</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;这里有个反例：假设&nbsp;<span class="inlinecode"><span class="id" type="var">subst_equiv_property</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;成立能够让我们证明以下两个程序等价...&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> <span class="id" type="var">c<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1)%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> <span class="id" type="var">c<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>) <span class="id" type="tactic">by</span> (<span class="id" type="tactic">subst</span>; <span class="id" type="tactic">apply</span> <span class="id" type="var">Contra</span>).<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;...我们来证明&nbsp;<span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span>&nbsp;能够在两个不同的状态下停机：<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;st<sub>1</sub>&nbsp;=&nbsp;(Y&nbsp;!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;1&nbsp;;&nbsp;X&nbsp;!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;1)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;st<sub>2</sub>&nbsp;=&nbsp;(Y&nbsp;!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;2&nbsp;;&nbsp;X&nbsp;!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;1).&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">Y</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 1 ; <span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 1) <span class="id" type="keyword">as</span> <span class="id" type="var">st<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">Y</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 2 ; <span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 1) <span class="id" type="keyword">as</span> <span class="id" type="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">empty_st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st<sub>1</sub></span>);<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">empty_st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st<sub>2</sub></span>);<br/>
&nbsp;&nbsp;<span class="id" type="tactic">try</span> (<span class="id" type="tactic">subst</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Seq</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := (<span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 1));<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>1</sub></span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;最后，因为程序求值的确定性而产生矛盾。&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Hcontra</span> : <span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">by</span> (<span class="id" type="tactic">apply</span> (<span class="id" type="var">ceval_deterministic</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">empty_st</span>); <span class="id" type="tactic">assumption</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Hcontra'</span> : <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">Y</span> = <span class="id" type="var">st<sub>2</sub></span> <span class="id" type="var">Y</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">by</span> (<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hcontra</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">subst</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">Hcontra'</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab35"></a><h4 class="section">练习：4 星, standard, optional (better_subst_equiv)</h4>
 之前我们思考的等价关系也不全是妄言 &mdash; 只要再增加一个条件，
    即变量 <span class="inlinecode"><span class="id" type="var">X</span></span> 不在第一个赋值语句的右边出现，它就是正确的了。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">var_not_used_in_aexp</span> (<span class="id" type="var">x</span> : <span class="id" type="var">string</span>) : <span class="id" type="var">aexp</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">VNUNum</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> (<span class="id" type="var">ANum</span> <span class="id" type="var">n</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">VNUId</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">y</span>, <span class="id" type="var">x</span> ≠ <span class="id" type="var">y</span> → <span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> (<span class="id" type="var">AId</span> <span class="id" type="var">y</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">VNUPlus</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> (<span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">VNUMinus</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> (<span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">VNUMult</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> (<span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">aeval_weakening</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">st</span> <span class="id" type="var">a</span> <span class="id" type="var">ni</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">aeval</span> (<span class="id" type="var">x</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">ni</span> ; <span class="id" type="var">st</span>) <span class="id" type="var">a</span> = <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
使用 <span class="inlinecode"><span class="id" type="var">var_not_used_in_aexp</span></span>，形式化并证明正确版本的 <span class="inlinecode"><span class="id" type="var">subst_equiv_property</span></span>。 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab36"></a><h4 class="section">练习：3 星, standard (inequiv_exercise)</h4>
 证明无限循环不等价于 <span class="inlinecode"><span class="id" type="var">SKIP</span></span> 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">inequiv_exercise</span>:<br/>
&nbsp;&nbsp;¬<span class="id" type="var">cequiv</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">true</span> <span class="id" type="var">DO</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">END</span>) <span class="id" type="var">SKIP</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab37"></a><h1 class="section">扩展练习：非确定性 Imp</h1>

<div class="paragraph"> </div>

 正如之前所见（<span class="inlinecode"><span class="id" type="var">Imp</span></span> 一章中的 <span class="inlinecode"><span class="id" type="var">ceval_deterministic</span></span>），Imp
    的求值关系是确定性的。然而在一些实际的编程语言定义中，<b>非确定性</b>
    也是十分重要的一部分。例如，在很多指令式语言中（如 C 系的语言），
    函数参数的求值顺序是未指定的。程序片段

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">x</span>&nbsp;=&nbsp;0;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">f</span>(++<span class="id" type="var">x</span>,&nbsp;<span class="id" type="var">x</span>)
<div class="paragraph"> </div>

</div>
    调用 <span class="inlinecode"><span class="id" type="var">f</span></span> 时所用的参数可能是 <span class="inlinecode">(1,</span> <span class="inlinecode">0)</span> 或者 <span class="inlinecode">(1,</span> <span class="inlinecode">1)</span>，取决于编译器的选择。
    这可能会让程序员感到困惑，但给了编译器作者选择实现的自由。

<div class="paragraph"> </div>

    在此练习中，我们会用一个简单的非确定性指令来扩展 Imp，
    研究这种改变会对程序等价关系产生何种影响。新指令的语法为 <span class="inlinecode"><span class="id" type="var">HAVOC</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>，
    其中 <span class="inlinecode"><span class="id" type="var">X</span></span> 是一个标识符。执行 <span class="inlinecode"><span class="id" type="var">HAVOC</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> 会为变量 <span class="inlinecode"><span class="id" type="var">X</span></span> 赋予一个不确定的
    <b>任意</b> 数值。例如，在执行完程序

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">HAVOC</span>&nbsp;<span class="id" type="var">Y</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Z</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;*&nbsp;2
<div class="paragraph"> </div>

</div>
    后，<span class="inlinecode"><span class="id" type="var">Y</span></span> 的值可以是任何数，而 <span class="inlinecode"><span class="id" type="var">Z</span></span> 的值是 <span class="inlinecode"><span class="id" type="var">Y</span></span> 的两倍（因此 <span class="inlinecode"><span class="id" type="var">Z</span></span> 总是偶数）。
    注意，我们并未讨论输出值的<b>概率</b>，在执行完此非确定性代码后，
    会有无穷多可能的不同输出。

<div class="paragraph"> </div>

    某种意义上来说，<span class="inlinecode"><span class="id" type="var">HAVOC</span></span> 所作用的变量大致相当于 C 之类的低级语言中的
    未初始化变量。经过了 <span class="inlinecode"><span class="id" type="var">HAVOC</span></span> 的变量会保存一个固定但任意的数值。
    语言定义中的大部分非确定性来源于程序员对语言所做的选择不那么关心
    （好处是能让编译器选择更快的运行方式）。

<div class="paragraph"> </div>

    我们称这个心语言为<b>Himp</b>（“用 <span class="inlinecode"><span class="id" type="var">HAVOC</span></span> 扩展的 Imp”）。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">Himp</span>.<br/>
</div>

<div class="doc">
为了形式化 Himp，我们首先在指令定义中增加一条从句。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">com</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">CSkip</span> : <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CAss</span> : <span class="id" type="var">string</span> → <span class="id" type="var">aexp</span> → <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CSeq</span> : <span class="id" type="var">com</span> → <span class="id" type="var">com</span> → <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CIf</span> : <span class="id" type="var">bexp</span> → <span class="id" type="var">com</span> → <span class="id" type="var">com</span> → <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CWhile</span> : <span class="id" type="var">bexp</span> → <span class="id" type="var">com</span> → <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CHavoc</span> : <span class="id" type="var">string</span> → <span class="id" type="var">com</span>. <span class="comment">(*&nbsp;&lt;---&nbsp;新增&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "'SKIP'" :=<br/>
&nbsp;&nbsp;<span class="id" type="var">CSkip</span> : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "X '<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>' a" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CAss</span> <span class="id" type="var">X</span> <span class="id" type="var">a</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 60) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "c<sub>1</sub> ;; c<sub>2</sub>" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CSeq</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "'WHILE' b 'DO' c 'END'" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CWhile</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "'TEST' e<sub>1</sub> 'THEN' e<sub>2</sub> 'ELSE' e<sub>3</sub> 'FI'" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CIf</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">e<sub>3</sub></span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "'HAVOC' l" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CHavoc</span> <span class="id" type="var">l</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 60) : <span class="id" type="var">imp_scope</span>.<br/>
</div>

<div class="doc">
<a name="lab38"></a><h4 class="section">练习：2 星, standard (himp_ceval)</h4>
 现在，我们必须扩展操作语义。前面我们已经提过了 <span class="inlinecode"><span class="id" type="var">ceval</span></span> 关系的模版，
    指定了大步语义。为了形式化 <span class="inlinecode"><span class="id" type="var">HAVOC</span></span> 指令的行为，我们还需要在 <span class="inlinecode"><span class="id" type="var">ceval</span></span>
    的定义中添加哪些规则？ 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Reserved Notation</span> "st '=[' c ']⇒' st'" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ceval</span> : <span class="id" type="var">com</span> → <span class="id" type="var">state</span> → <span class="id" type="var">state</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Skip</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">SKIP</span> ]⇒ <span class="id" type="var">st</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Ass</span>  : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">n</span> <span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span> = <span class="id" type="var">n</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span> ]⇒ (<span class="id" type="var">x</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">n</span> ; <span class="id" type="var">st</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Seq</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">st''</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st'</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st''</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">c<sub>1</sub></span> ;; <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st''</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_IfTrue</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span> ]⇒ <span class="id" type="var">st'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_IfFalse</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">false</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span> ]⇒ <span class="id" type="var">st'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_WhileFalse</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">st</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">false</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_WhileTrue</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">st''</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st'</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st''</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st''</span><br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
<br/>
&nbsp;&nbsp;<span class="id" type="keyword">where</span> "st =[ c ]⇒ st'" := (<span class="id" type="var">ceval</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>).<br/>
<span class="id" type="var">Close</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span>.<br/>
</div>

<div class="doc">
作为合理性检查，以下断言对于你的定义来说应该是可证的： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">havoc_example1</span> : <span class="id" type="var">empty_st</span> =[ (<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span> ]⇒ (<span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 0).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">havoc_example2</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">empty_st</span> =[ (<span class="id" type="var">SKIP</span>;; <span class="id" type="var">HAVOC</span> <span class="id" type="var">Z</span>)%<span class="id" type="var">imp</span> ]⇒ (<span class="id" type="var">Z</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 42).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_Check_rule_for_HAVOC</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 最后，我们重新定义和之前等价的指令： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">cequiv</span> (<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span> := <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> : <span class="id" type="var">state</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span> ↔ <span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>.<br/>
</div>

<div class="doc">
我们应用此定义来证明一些非确定性程序是否等价。 
<div class="paragraph"> </div>

<a name="lab39"></a><h4 class="section">练习：3 星, standard (havoc_swap)</h4>
 以下两个程序是否等价？ 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">pXY</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>;; <span class="id" type="var">HAVOC</span> <span class="id" type="var">Y</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">pYX</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">HAVOC</span> <span class="id" type="var">Y</span>;; <span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span>.<br/>
</div>

<div class="doc">
请证明你的想法。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pXY_cequiv_pYX</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">pXY</span> <span class="id" type="var">pYX</span> ∨ ¬<span class="id" type="var">cequiv</span> <span class="id" type="var">pXY</span> <span class="id" type="var">pYX</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab40"></a><h4 class="section">练习：4 星, standard, optional (havoc_copy)</h4>
 以下两个程序是否等价？ 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">ptwice</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>;; <span class="id" type="var">HAVOC</span> <span class="id" type="var">Y</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">pcopy</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>;; <span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span>.<br/>
</div>

<div class="doc">
请证明你的想法。（提示：你可能会用到 <span class="inlinecode"><span class="id" type="tactic">assert</span></span> 的略。） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ptwice_cequiv_pcopy</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">ptwice</span> <span class="id" type="var">pcopy</span> ∨ ¬<span class="id" type="var">cequiv</span> <span class="id" type="var">ptwice</span> <span class="id" type="var">pcopy</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 我们在这里使用的程序等价关系的定义对无限循环的程序来说有点复杂。因为
    <span class="inlinecode"><span class="id" type="var">cequiv</span></span> 描述的是两个等价的程序在<b>停机</b>时输出的集合是相同的。然而，
    在像 Himp 这类带有非确定的语言中，有些程序总会停机，有些程序总会发散，
    还有些程序会非确定地在某些时候停机而在其它时候发散。
    以下练习的最后一部分展示了这种现象。

<div class="paragraph"> </div>

<a name="lab41"></a><h4 class="section">练习：4 星, advanced (p1_p2_term)</h4>
 考虑一下指令： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>1</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ¬(<span class="id" type="var">X</span> = 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">HAVOC</span> <span class="id" type="var">Y</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>2</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ¬(<span class="id" type="var">X</span> = 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/>
</div>

<div class="doc">
直觉上来说，<span class="inlinecode"><span class="id" type="var">p<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">p<sub>2</sub></span></span> 的停机行为相同：要么无限循环，要么以相同的状态开始，
    就在相同的状态下停机。我们可以用以下引理分别刻画 <span class="inlinecode"><span class="id" type="var">p<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">p<sub>2</sub></span></span> 的停机行为： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">p1_may_diverge</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span>, <span class="id" type="var">st</span> <span class="id" type="var">X</span> ≠ 0 →<br/>
&nbsp;&nbsp;¬<span class="id" type="var">st</span> =[ <span class="id" type="var">p<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">p2_may_diverge</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span>, <span class="id" type="var">st</span> <span class="id" type="var">X</span> ≠ 0 →<br/>
&nbsp;&nbsp;¬<span class="id" type="var">st</span> =[ <span class="id" type="var">p<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab42"></a><h4 class="section">练习：4 星, advanced (p1_p2_equiv)</h4>
 使用这两个引理来证明 <span class="inlinecode"><span class="id" type="var">p<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">p<sub>2</sub></span></span> 确实等价。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">p1_p2_equiv</span> : <span class="id" type="var">cequiv</span> <span class="id" type="var">p<sub>1</sub></span> <span class="id" type="var">p<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab43"></a><h4 class="section">练习：4 星, advanced (p3_p4_inequiv)</h4>
 证明以下程序<b>不等价</b>（提示：当 <span class="inlinecode"><span class="id" type="var">p<sub>3</sub></span></span> 停机时 <span class="inlinecode"><span class="id" type="var">Z</span></span> 的值是什么？当
    <span class="inlinecode"><span class="id" type="var">p<sub>4</sub></span></span> 停机时呢？） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>3</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 1;;<br/>
&nbsp;&nbsp;<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">HAVOC</span> <span class="id" type="var">Z</span><br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>4</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0;;<br/>
&nbsp;&nbsp;<span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 1)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">p3_p4_inequiv</span> : ¬<span class="id" type="var">cequiv</span> <span class="id" type="var">p<sub>3</sub></span> <span class="id" type="var">p<sub>4</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab44"></a><h4 class="section">练习：5 星, advanced, optional (p5_p6_equiv)</h4>
 证明以下指令等价。（提示：正如我们之前提到的，我们为 Himp 定义的
    <span class="inlinecode"><span class="id" type="var">cequiv</span></span> 只考虑了可能的停机配置的集合：对于两个拥有相同起始状态 <span class="inlinecode"><span class="id" type="var">st</span></span>
    的程序而言，当且仅当二者可能的停机状态的集合相同时，二者才等价。
    若 <span class="inlinecode"><span class="id" type="var">p<sub>5</sub></span></span> 停机，那么最终状态应当是什么？反过来说，<span class="inlinecode"><span class="id" type="var">p<sub>5</sub></span></span> 总是会停机吗？） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>5</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = 1) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span><br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>6</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 1)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">p5_p6_equiv</span> : <span class="id" type="var">cequiv</span> <span class="id" type="var">p<sub>5</sub></span> <span class="id" type="var">p<sub>6</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">Himp</span>.<br/>
</div>

<div class="doc">
<a name="lab45"></a><h1 class="section">附加练习</h1>

<div class="paragraph"> </div>

<a name="lab46"></a><h4 class="section">练习：4 星, standard, optional (for_while_equiv)</h4>
 此练习是 <a href="https://coq-zh.github.io/SF-zh/lf-current/Imp.html"><span class="inlineref">Imp</span></a> 一章中可选练习 <span class="inlinecode"><span class="id" type="var">add_for_loop</span></span> 的扩展，
    就是那个让你扩展出类似 C 风格的 <span class="inlinecode"><span class="id" type="keyword">for</span></span> 循环指令的练习。请证明指令：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">for</span>&nbsp;(<span class="id" type="var">c<sub>1</sub></span>&nbsp;;&nbsp;<span class="id" type="var">b</span>&nbsp;;&nbsp;<span class="id" type="var">c<sub>2</sub></span>)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>3</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;}
<div class="paragraph"> </div>

</div>
    等价于：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>1</sub></span>&nbsp;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">WHILE</span>&nbsp;<span class="id" type="var">b</span>&nbsp;<span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>3</sub></span>&nbsp;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab47"></a><h4 class="section">练习：3 星, standard, optional (swap_noninterfering_assignments)</h4>
 （提示：这里你需要 <span class="inlinecode"><span class="id" type="var">functional_extensionality</span></span>。） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">swap_noninterfering_assignments</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">l<sub>1</sub></span> ≠ <span class="id" type="var">l<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">l<sub>2</sub></span> <span class="id" type="var">a<sub>1</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">l<sub>1</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span>;; <span class="id" type="var">l<sub>2</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">l<sub>2</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>2</sub></span>;; <span class="id" type="var">l<sub>1</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab48"></a><h4 class="section">练习：4 星, advanced, optional (capprox)</h4>
 在这个练习中我们定义了一个非对称的程序等价变形, 叫做
    <b>程序近似（program approximation）</b>。 当每个能让 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>
    停机的初始状态也能让 <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> 在相同的状态下停机时，我们就说程序 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>
    <b>近似与</b> 程序 <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> 。下面是程序近似的形式化定义： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">capprox</span> (<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span> := <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">st</span> <span class="id" type="var">st'</span> : <span class="id" type="var">state</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span> → <span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>.<br/>
</div>

<div class="doc">
例如，程序

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">c<sub>1</sub></span>&nbsp;=&nbsp;<span class="id" type="var">WHILE</span>&nbsp;~(<span class="id" type="var">X</span>&nbsp;=&nbsp;1)&nbsp;<span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;-&nbsp;1<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>
<div class="paragraph"> </div>

</div>
    近似于 <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> <span class="inlinecode">1</span>，但是 <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> 不近似于 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>，因为 <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>
    不会在 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span> 时停机，而 <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> 会。如果两个程序互相近似，那么它们等价。 
<div class="paragraph"> </div>

 请找出两个程序 <span class="inlinecode"><span class="id" type="var">c<sub>3</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">c<sub>4</sub></span></span>，它们互不近似。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">c<sub>3</sub></span> : <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">c<sub>4</sub></span> : <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">c3_c4_different</span> : ¬<span class="id" type="var">capprox</span> <span class="id" type="var">c<sub>3</sub></span> <span class="id" type="var">c<sub>4</sub></span> ∧ ¬<span class="id" type="var">capprox</span> <span class="id" type="var">c<sub>4</sub></span> <span class="id" type="var">c<sub>3</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
找出一个程序 <span class="inlinecode"><span class="id" type="var">cmin</span></span> 近似于所有别的程序。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">cmin</span> : <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">cmin_minimal</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span>, <span class="id" type="var">capprox</span> <span class="id" type="var">cmin</span> <span class="id" type="var">c</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
最后，再找出程序近似的一个非平凡的属性（当从左到右时）。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">zprop</span> (<span class="id" type="var">c</span> : <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">zprop_preserving</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">c'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">zprop</span> <span class="id" type="var">c</span> → <span class="id" type="var">capprox</span> <span class="id" type="var">c</span> <span class="id" type="var">c'</span> → <span class="id" type="var">zprop</span> <span class="id" type="var">c'</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:15:17&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>